g:Mon, b, b':, p:|g|. (when b. when b'. p) = (when b  b'. p)  |g| 

latex

Up	groups 1
Definitions of Statement	Mon, when b. p
Definitions	ff, tt, t  T, if b then t else f fi , p  q, when b. p, x:A. B(x), Unit, , Mon,
Lemmas	mon wf, bool wf, grp car wf, grp id wf